/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.prover;

import java.io.IOException;
import java.util.Collection;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Set;
import java.util.TreeSet;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;
import java.util.logging.Level;
import java.util.logging.Logger;

import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.prover.ProverResult.Status;

/**
 * Facade around SMT solver invocations that will take care of constructing
 * the actual SMT formula, invoking the solver, processing the result,
 * and enforcing timeouts if necessary.
 * TODO allow solvers other than Z3
 * @author kevin
 * @since Feb 7, 2010
 */
public class SmtLib implements Prover {

	private static final Logger log = Logger.getLogger(SmtLib.class.getName());

	private static final ExecutorService executor =
		Executors.newSingleThreadExecutor();

	private final boolean heapMapEncoding;
	private final IFieldInfo checker;
	private final Z3Factory proverFactory = new Z3Factory();
	private final int forceTimeoutSeconds;

	private String context = "";
	private long solverTime = 0;

	public SmtLib(IFieldInfo checker, boolean map) {
		this.checker = checker;
		this.heapMapEncoding = map;
		if (Boolean.getBoolean("javasyp.solver.dontKill"))
			// don't use executor if property set to "true" only (slightly faster)
			this.forceTimeoutSeconds = 0;
		else
			// kill process if it doesn't as promised (default, slightly slower)
			this.forceTimeoutSeconds = 1 + proverFactory.getTimeoutSeconds();
	}

	@Override
	public long getSolverMillis() {
		return solverTime;
	}

	public String getContext() {
		return context;
	}

	public void setContext(String context) {
		if (context == null)
			throw new IllegalArgumentException("null context");
		this.context = context;
	}

	@Override
	public ProverResult check(Collection<? extends Formula> assumptions, Formula query)
	throws InterruptedException {
		if (log.isLoggable(Level.INFO))
			log.info(context + ": " + query + " <== " + assumptions);
		SmtSolverZ3 smt = null;
		try {
			smt = createSolver();
			SmtLibFormatter format = createFormatter();
			StringBuilder check = new StringBuilder();

			// header
			smt.println("(benchmark b");
			smt.println("  :status unsat"); // expect unsat, since we negate
			/*
			 * "Closed formulas with free function and predicate symbols over
			 * a theory of arrays of arrays of integer index and real value."
			 * Seems to be the most permissive SMT-LIB logic
			 *
			 * Declared logic avoids Z3 crashes when no Int var has concrete value:
			 * (benchmark b
			 *    :status unsat
			 *    :extrafuns ((copyA Int))
			 *    :extrafuns ((this.a Int))
			 *    :extrafuns ((copyB Int))
			 *    :extrafuns ((this.b Int))
			 *    :extrafuns ((this.a17 Int))
			 *    :assumption (= copyA this.a)
			 *    :assumption (= copyB this.b)
			 *    :formula (not (= this.a17 copyA))
			 *  )
			 *  crashes with output (note Int-sorted symbols get abstract values):
			 *  this.a -> val!0
			 *  this.a17 -> val!1
			 *  this.b ->
			 */
			smt.println("  :logic AUFNIRA");

			// format formulas first to collect free variables
			for (Formula f : assumptions) {
				check.append(String.format("  :assumption %s%n", f.dispatch(format)));
			}
			// negate query formula only and expect unsat to get desired encoding
			// of forall assumptions ==> query as not exists assumtions & !query
			check.append(String.format("  :formula (not %s)", query.dispatch(format)));

			// print sorts before funs so SMT solver doesn't get confused
			for (String s : format.getExtraSorts()) {
				smt.println("  :extrasorts (" + s + ")");
			}

			// print free variables before formulas so SMT solver doesn't get confused
			for (String p : format.getExtraPreds()) {
				smt.println("  :extrapreds (" + p + ")");
			}

			// print free variables before formulas so SMT solver doesn't get confused
			for (String p : format.getExtraFuns()) {
				smt.println("  :extrafuns (" + p + ")");
			}

			// print axioms as assumptions (as we don't have "extraaxioms")
			for (String p : format.getAxioms()) {
				smt.println("  :assumption " + p);
			}

			// print encoded assumptions and query
			smt.println(check.toString());
			smt.println(")");

			Status status;
			long start = System.currentTimeMillis();
			Future<Status> z3task =
				forceTimeoutSeconds <= 0 ? null : executor.submit(smt);
			try {
				status = z3task == null ? smt.call() : z3task.get(forceTimeoutSeconds, TimeUnit.SECONDS);
			} catch (TimeoutException e) {
				// shouldn't happen as we also set timeout parameter in pbuilder
				// but Z3 sometimes seems to go crazy
				log.log(Level.WARNING, "SMT solver didn't time out on its own");
				// kill "rogue" process
				z3task.cancel(true);
				// TODO include SMT query in result
				return ProverResult.TIMEOUT;
			} catch (ExecutionException e) {
				// should already be dead but just in case
				z3task.cancel(true);
				final Throwable cause = e.getCause();
				if (cause instanceof IOException)
					// so we can use the same catch block with and without future
					throw (IOException) cause;
				if (cause instanceof RuntimeException)
					// so runtime exceptions behave the same with and without future
					throw (RuntimeException) cause;
				// shouldn't get here unless someone adds checked exceptions to smt.call()
				log.log(Level.SEVERE, "Unexpected checked exception from solver invocation", cause);
				return new Z3Result(smt, cause);
			} finally {
				solverTime += (System.currentTimeMillis() - start);
			}
			if (status == Status.UNSAT && smt.getMessages() == null)
				return ProverResult.UNSAT;
			else
				return new Z3Result(smt, status);
		} catch (IOException e) {
			log.log(Level.SEVERE, "Error invoking SMT solver", e);
			return new Z3Result(smt, e);
		}
	}

	private SmtLibFormatter createFormatter() {
		return new SmtLibFormatter(checker, heapMapEncoding);
	}

	private SmtSolverZ3 createSolver() throws IOException {
		return proverFactory.create();
	}

	private final static class Z3Result extends ProverResult {

		private final String z3messages;
		private final Map<String, ? extends Object> z3model;
		private final String smtQuery;
		private Set<String> counterexample;

		/**
		 * @param status
		 * @param z3
		 */
		private Z3Result(SmtSolverZ3 z3, Status status) {
			super(status);
			this.z3messages = z3.getMessages();
			this.z3model = z3.getModel();
			this.smtQuery = z3.getQuery();
		}

		/**
		 * Creates an {@link Status#OTHER} result for the given exception
		 * that includes {@link SmtSolverZ3#getMessages()}, if any.
		 * @param t
		 * @param z3
		 */
		private Z3Result(SmtSolverZ3 z3, Throwable t) {
			super(Status.OTHER);
			StringBuilder msg = new StringBuilder();
			msg.append(t.getClass().getSimpleName())
				.append(": ")
				.append(t.getLocalizedMessage());
			if (z3 != null && z3.getMessages() != null)
				msg.append("\n").append(z3.getMessages());
			this.z3messages = msg.toString();
			this.z3model = null;
			this.smtQuery = z3.getQuery();
		}

		@Override
		public String getQuery() {
			return smtQuery;
		}

		@Override
		public Collection<? extends String> getCounterExample() {
			if (counterexample != null || z3model == null)
				return counterexample;

			counterexample = new TreeSet<String>();

			Map<String, String> backMap = new HashMap<String, String>();
			Map<String, Integer> latest = new LinkedHashMap<String, Integer>();
			for (Map.Entry<String, ? extends Object> m : z3model.entrySet()) {
				Object v = m.getValue();
				if (v instanceof String) {
					String s = (String) v;
					if (s.startsWith("val!")) {
						String oldVal = backMap.put(s, m.getKey());
						if (oldVal != null)
							counterexample.add(oldVal + " = " + m.getKey());
						continue;
					}
				}
				String h = m.getKey();
				if ("final".equals(h))
					// ignore "final" predicate
					continue;
				int p = h.length();
				while (0 < p && Character.isDigit(h.charAt(p - 1)))
					--p;
				Integer i = h.length() - p <= 0 ? null : Integer.valueOf(h.substring(p));
				String obj = h.substring(0, p);
				if ("temp".equals(obj))
					// show all temps TODO distinguish temps from variables called "temp"
					latest.put(h, null);
				else if (latest.get(obj) == null || (i != null && latest.get(obj) < i))
					// show only latest incarnation of locals
					latest.put(obj, i);
			}

			StringBuilder helper = new StringBuilder();
			for (Map.Entry<String, Integer> l : latest.entrySet()) {
				String var = l.getKey();
				String id = var + (l.getValue() == null ? "" : l.getValue());
				Object v = z3model.get(id);
				if (v instanceof Map<?, ?>) {
					@SuppressWarnings("unchecked") Map<String, ? extends Object> heap =
						(Map<String, ? extends Object>) v;
					boolean isArrayHeap = var.startsWith("select");
					heap:
					for (Map.Entry<String, ? extends Object> cell : heap.entrySet()) {
						String c = cell.getKey().trim();
						helper.delete(0, helper.length());
						if ("else".equals(c)) {
							// skip "else" values as they don't seem to be relevant
							continue heap;
//							helper.append(var).append(isArrayHeap ? "[else]" : ".else");
						} else {
							String[] path = cell.getKey().split("\\s+");
							boolean first = true;
							for (String p : path) {
								if (p.isEmpty())
									continue;
								if (!first)
									helper.append(isArrayHeap ? '[' : '.');
								String segment = getSourceValue(p, backMap);
								if (1 < path.length && "null".equals(segment))
									// skip null dereferences
									continue heap;
								helper.append(segment);
								if (!first & isArrayHeap) {
									try {
										int idx = Integer.parseInt(p);
										// skip negative array indices
										if (idx < 0)
											continue heap;
										// TODO skip indices beyond array length
									} catch (NumberFormatException e) { /* ignore */ }
									helper.append(']');
								}
								first = false;
							}
						}
						helper.append(" = ").append(getSourceValue(cell.getValue(), backMap));
						counterexample.add(helper.toString());
					}
				} else {
					while (var.endsWith("!"))
						var = var.substring(0, var.length() - 1);
					// TODO somehow show the expressions temps stand for
					counterexample.add(var + " = " + getSourceValue(v, backMap));
				}
			}

			return counterexample;
		}

		public String getSourceValue(Object v, Map<String, String> backMap) {
			String val = v.toString();
			String back = backMap.get(val);
			return back == null ? val : back;
		}

		@Override
		public String getWarnings() {
			return z3messages;
		}
	}
}
